 $LOAD_PATH.unshift File.join(File.dirname(__FILE__),'../..','ext_pr1/lib')
 require 'ext_pr1_v4'

class Object
  #####################Typprädikate#############################
  def dim1?() (point1d? or range1d? or union1d? or shape1d?) end
  def dim2?() (point2d? or range2d? or union2d? or shape2d?) end
  def point1d?() false end
  def point2d?() false end
  def range1d?() false end
  def range2d?() false end
  def union1d?() false end
  def union2d?() false end
#Shape1d ::= Range1d | Union1d

def shape1d?()
 self.range1d? or self.union1d?
end

#Shape2d ::= Range2d | Union2d

def shape2d?()
  self.range2d? or self.union2d?
end

#UnionShape ::= Union1d | Union2d

def union_shape?()
  self.union1d? or self.union2d?
end

#GraphObj ::= Point | Shape

def graph_obj?()
  self.point? or self.shape?
end

#Point ::= Point1d | Point2d

def point?()
  self.point1d? or self.point2d?
end

#Shape ::= PrimShape | CompShape

def shape?()
  self.prim_shape? or self.comp_shape?
end

#CompShape ::= UnionShape

def comp_shape?()
  self.union_shape?
end

#PrimShape ::= Range1d | Range2d

def prim_shape?()
    self.range1d? or self.range2d?
end
end
 #Fehlerbehebung weil er die find_min und find_max Methoden sonst nicht findet
class Integer
  def find_min(r2) self < r2 ? self : r2 end
  def find_max(r2) self < r2 ? r2 : self end
end
#Datendefinitionen:
#
#1D Objekte
#
#Point1d ::= Int
 
class Point1d
  

def initialize(int)
    @int = int
  end
  
  def point1d?()
    true
  end
  
  def int()
    @int
  end
  
  def ==(o) 
    self.equal?(o) or (o.graph_obj? and (int == o.int)) 
  end
  
  def to_s
    'Point1d'+'['+(int.to_s)+']'
  end
  
  def self.[](*args) check_inv(self.new(*args)) end
  
  def invariant?() 
    @int.int?
  end

  #translate ::= (shape, point) :: Shape x Point ->? Shape

def translate(point)
  check_pre((point.point1d?))
    self.trans0d(point)
end

#trans0d ::= (point1, point2) :: Point1d x Point1d -> Point1d

def trans0d(point)  
  Point1d[self.int + point.int]
end

#VERSION 1:
#
#graph_equal? ::= (o1,o2) :: GraphObj x GraphObj ->? Bool
#(o1.point1d? and o2.point1d?) or
#      (o1.point2d? and o2.point2d?) or 
#      (shape1d?(o1) and shape1d?(o2)) or
#      (shape2d?(o1) and shape2d?(o2)) then
#      o1 == o2
def graph_equal_?(o2)
 check_pre((o2.graph_obj?))
 (o2.point1d?) ? (self.int == o2.int) : false
end

#
#VERSION 2:
#
#graph_equal? ::= (o1,o2) :: Any x Any ->? Bool

def graph_equal?(o2)
 if (self.graph_obj? and o2.graph_obj?) then
 self.graph_equal_?(o2)
 elsif (self.graph_obj? or o2.graph_obj?) then
  check_pre(false)
 else
  false
 end
end

#graph_equal_trans? ::= (o1,o2) :: Any x Any ->? Bool

def graph_equal_trans?(o2) o2.dim1? end


#in? ::= (point, shape) :: Point x Shape -> Bool
def in?(val)
  check_pre((val.shape1d?))
  val.range1d? ? int.between?(val.first.int, val.last.int) : val.union1d? ? val.bounds().in?() : false
end
end
#Range1d ::= Range[first,last] :: Point1d x Point1d

class Range1d

  def initialize(first, last)
    @first = first
    @last = last
  end
  
  def range1d?() true end
  
  def first() @first end
  
  def last() @last end
  
  def ==(o) 
    self.equal?(o) or (o.graph_obj? and (first == o.first) and (last == o.last)) 
  end
  
  def to_s
    'Range1d'+'['+ first.to_s + ', ' + last.to_s + ']'
  end
  
  def self.[](*args) check_inv(self.new(*args)) end
  
  def invariant?()
    @first.point1d?
    @last.point1d?
  end
  
  #translate ::= (shape, point) :: Shape x Point ->? Shape

def translate(point)
 check_pre((point.point1d?))
Range1d[self.first.trans0d(point), self.last.trans0d(point)]
end

#bounding_range ::= (r1,r2) :: (Range1d x Range1d) -> Range1d | (Range2d x Range2d) -> Range2d

def bounding_range(r2)
check_pre((r2.range1d?))
      first = (self.first.int).find_min(r2.first.int)
      last = (self.last.int).find_max(r2.last.int)
      Range1d[Point1d[first],Point1d[last]]
end

def bounds()
  self
end
#VERSION 1:
#
#graph_equal? ::= (o1,o2) :: GraphObj x GraphObj ->? Bool
def graph_equal_?(o2)
 o2.range1d? ? (length() == o2.length()) : o2.poin1d? ? (o2.point1d.int == self.last.int and self.last.int == self.first.int) : false
end

def length()
  self.last.int - self.first.int
end
#
#VERSION 2:
#
#graph_equal? ::= (o1,o2) :: Any x Any ->? Bool

def graph_equal?(o2)
 o2.graph_obj? ? graph_equal_?(o2) : false
end

#graph_equal_trans? ::= (o1,o2) :: Any x Any ->? Bool

def graph_equal_trans?(o2)
o2.dim1? ? graph_equal?(o2) : false
end
end
#Union1d ::= Union1d[left,right] :: Shape1d x Shape1d

class Union1d

  def initialize(left, right)
    @left = left
    @right = right
  end
  
  def union1d?()
  true
  end
  
  def left()
    @left
  end
  
  def right()
    @right
  end
  
  def ==(o) 
    self.equal?(o) or (o.graph_obj? and (left == o.left) and (right == o.right)) 
  end
  
  def to_s
    'Union1d'+'['+(left.to_s) + ', ' + right.to_s + ']'
  end
  
  def self.[](*args) check_inv(self.new(*args)) end
  
  def invariant?()
    shape1d?()
  end
  
   #Shape1d ::= Range1d | Union1d

def shape1d?()
 (self.left.range1d? or self.left.union1d?) and (self.right.range1d? or self.right.union1d?)
end

  #translate ::= (shape, point) :: Shape x Point ->? Shape

def translate(point)
  check_pre((point.point1d?))
  Union1d[left.bounds().translate(point), right.bounds().translate(point)]
end

#bounds ::= (shape) :: Shape -> (Range1d | Range2d)

def bounds()
 (self.left).bounding_range(self.right)     
end
#VERSION 1:
#
#graph_equal? ::= (o1,o2) :: GraphObj x GraphObj ->? Bool
def graph_equal_?(o2)
(o2.union1d?) ? (left.bounds().graph_equal_?(o2.left.bounds()) == right.bounds().graph_equal_?(o2.right.bounds())) : false
end
#
#VERSION 2:
#
#graph_equal? ::= (o1,o2) :: Any x Any ->? Bool

def graph_equal?(o2)
 o2.graph_obj? ? graph_equal_?(o2) : false
end

#graph_equal_trans? ::= (o1,o2) :: Any x Any ->? Bool

def graph_equal_trans?(o2)
o2.dim1? ? graph_equal?(o2) : false
end
end
#2D Objekte
#
#Point2d :: = Point2d[x,y] :: Point1d x Point1d

class Point2d

 def initialize(x, y)
    @x = x
    @y = y
  end
  
  def point2d?()
    true
  end
  
  def x()
    @x
  end
  
  def y()
    @y
  end
  
  def ==(o) 
    self.equal?(o) or (o.graph_obj? and (x == o.x) and y == o.y) 
  end
  
  def to_s
    'Point2d' + '[' + x.to_s + ', ' + y.to_s + ']'
  end
  
  def self.[](*args) check_inv(self.new(*args)) end
  
  def invariant?()
   @x.point1d?
   @y.point1d?
  end
 
  #translate ::= (shape, point) :: Shape x Point ->? Shape

def translate(point)
check_pre((point.point2d?))
Point2d[(self.x).translate(point.x), (self.y).translate(point.y)]
end

#VERSION 1:
#
#graph_equal? ::= (o1,o2) :: GraphObj x GraphObj ->? Bool
#(o1.point1d? and o2.point1d?) or
#      (o1.point2d? and o2.point2d?) or 
#      (shape1d?(o1) and shape1d?(o2)) or
#      (shape2d?(o1) and shape2d?(o2)) then
#      o1 == o2
def graph_equal_?(o2)
 check_pre((o2.graph_obj?))
 (o2.point2d?) ? (self.x.graph_equal_?(o2.x) and self.y.graph_equal_?(o2.y)) : false
end

#
#VERSION 2:
#
#graph_equal? ::= (o1,o2) :: Any x Any ->? Bool
def graph_equal?(o2)
 o2.graph_obj? ? graph_equal_?(o2) : false
end

#graph_equal_trans? ::= (o1,o2) :: Any x Any ->? Bool

def graph_equal_trans?(o2) o2.point2d? end

#in? ::= (point, shape) :: Point x Shape -> Bool
def in?(val)
check_pre((val.shape2d?))
 val.range2d? ? (self.x.in?(val.x_range) and self.y.in?(val.y_range)) : val.union2d? ? val.bounds().in?() : false
end
end
#Range2d ::= Range2d[x_range,y_range] :: (Range1d x Range1d)

class Range2d

 def initialize(x_range, y_range)
    @x_range = x_range
    @y_range = y_range
  end
  
  def range2d?()
  true
  end
  
  def x_range()
    @x_range
  end
  
  def y_range()
    @y_range
  end
  
  def ==(o) 
    self.equal?(o) or (o.graph_obj? and (x_range == o.x_range) and (y_range == o.y_range)) 
  end
  
  def to_s
    'Range2d' + '[' + x_range.to_s + ', ' + y_range.to_s + ']'
  end
  
  def self.[](*args) check_inv(self.new(*args)) end
  
 def invariant?()
   @x_range.range1d?
   @y_range.range1d?
 end
 
  #translate ::= (shape, point) :: Shape x Point ->? Shape

def translate(point)
check_pre((point.point2d?))
Range2d[self.x_range.translate(point.x), self.y_range.translate(point.y)]
end

#bounding_range ::= (r1,r2) :: (Range1d x Range1d) -> Range1d | (Range2d x Range2d) -> Range2d

def bounding_range(r2)
Range2d[self.x_range.bounding_range(r2.x_range), self.y_range.bounding_range(r2.y_range)]
end

#bounds ::= (shape) :: Shape -> (Range1d | Range2d)

def bounds()
  self
end

#VERSION 1:
#
#graph_equal? ::= (o1,o2) :: GraphObj x GraphObj ->? Bool
def graph_equal_?(o2)
 o2.range2d? ? (self.x_range.graph_equal_?(o2.x_range) and self.y_range.graph_equal_?(o2.y_range)) : false
end

#
#VERSION 2:
#
#graph_equal? ::= (o1,o2) :: Any x Any ->? Bool

def graph_equal?(o2)
 o2.graph_obj? ? graph_equal_?(o2) : false
end

#graph_equal_trans? ::= (o1,o2) :: Any x Any ->? Bool

def graph_equal_trans?(o2)
if (o2.range2d?) then
 self.graph_equal_?(o2)
else
  false
end
end
end
#Union2d ::= Union2d[left,right] :: Shape2d x Shape2d

class Union2d

  def initialize(left, right)
    @left = left
    @right = right
  end
  
  def union2d?()
  true
  end
  
  def left()
    @left
  end
  
  def right()
    @right
  end
  
  def ==(o) 
    self.equal?(o) or (o.graph_obj? and (left == o.left) and (right == o.right)) 
  end
  
  def to_s
    'Union2d'+'[' + left.to_s + ', '+ right.to_s + ']'
  end
  
  def self.[](*args) check_inv(self.new(*args)) end
  
 def invariant?()
   shape2d?()  
 end
 
#Shape2d ::= Range2d | Union2d

def shape2d?()
  (self.left.range2d? or self.left.union2d?) and (self.right.range2d? or self.right.union2d?)
end

  #translate ::= (shape, point) :: Shape x Point ->? Shape

def translate(point)
  check_pre((point.point2d?))
  Union2d[left.translate(point), right.translate(point)]
end

#bounds ::= (shape) :: Shape -> (Range1d | Range2d)

def bounds()
(self.left).bounding_range(self.right)
end

#VERSION 1:
#
#graph_equal? ::= (o1,o2) :: GraphObj x GraphObj ->? Bool
def graph_equal_?(o2)
check_pre((o2.graph_obj?))
(o2.union2d?) ? (left.bounds().graph_equal_?(o2.left.bounds()) == right.bounds().graph_equal_?(o2.right.bounds())) : false
end
#
#VERSION 2:
#
#graph_equal? ::= (o1,o2) :: Any x Any ->? Bool

def graph_equal?(o2)
 o2.graph_obj? ? graph_equal_?(o2) : false
end

#graph_equal_trans? ::= (o1,o2) :: Any x Any ->? Bool

def graph_equal_trans?(o2)
check_pre((o2.graph_obj?))
(o2.union2d?) ? self.graph_equal_?(o2) : false
end
end